0 CpxRelTRS
↳1 RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 9 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 32 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 715 ms)
↳12 BOUNDS(1, n^2)
*(@x, @y) → #mult(@x, @y)
dyade(@l1, @l2) → dyade#1(@l1, @l2)
dyade#1(::(@x, @xs), @l2) → ::(mult(@x, @l2), dyade(@xs, @l2))
dyade#1(nil, @l2) → nil
mult(@n, @l) → mult#1(@l, @n)
mult#1(::(@x, @xs), @n) → ::(*(@n, @x), mult(@n, @xs))
mult#1(nil, @n) → nil
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
*(@x, @y) → #mult(@x, @y) [1]
dyade(@l1, @l2) → dyade#1(@l1, @l2) [1]
dyade#1(::(@x, @xs), @l2) → ::(mult(@x, @l2), dyade(@xs, @l2)) [1]
dyade#1(nil, @l2) → nil [1]
mult(@n, @l) → mult#1(@l, @n) [1]
mult#1(::(@x, @xs), @n) → ::(*(@n, @x), mult(@n, @xs)) [1]
mult#1(nil, @n) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| * => times |
times(@x, @y) → #mult(@x, @y) [1]
dyade(@l1, @l2) → dyade#1(@l1, @l2) [1]
dyade#1(::(@x, @xs), @l2) → ::(mult(@x, @l2), dyade(@xs, @l2)) [1]
dyade#1(nil, @l2) → nil [1]
mult(@n, @l) → mult#1(@l, @n) [1]
mult#1(::(@x, @xs), @n) → ::(times(@n, @x), mult(@n, @xs)) [1]
mult#1(nil, @n) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
times(@x, @y) → #mult(@x, @y) [1]
dyade(@l1, @l2) → dyade#1(@l1, @l2) [1]
dyade#1(::(@x, @xs), @l2) → ::(mult(@x, @l2), dyade(@xs, @l2)) [1]
dyade#1(nil, @l2) → nil [1]
mult(@n, @l) → mult#1(@l, @n) [1]
mult#1(::(@x, @xs), @n) → ::(times(@n, @x), mult(@n, @xs)) [1]
mult#1(nil, @n) → nil [1]
#add(#0, @y) → @y [0]
#add(#neg(#s(#0)), @y) → #pred(@y) [0]
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) [0]
#add(#pos(#s(#0)), @y) → #succ(@y) [0]
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) [0]
#mult(#0, #0) → #0 [0]
#mult(#0, #neg(@y)) → #0 [0]
#mult(#0, #pos(@y)) → #0 [0]
#mult(#neg(@x), #0) → #0 [0]
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) [0]
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #0) → #0 [0]
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) [0]
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) [0]
#natmult(#0, @y) → #0 [0]
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) [0]
#pred(#0) → #neg(#s(#0)) [0]
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) [0]
#pred(#pos(#s(#0))) → #0 [0]
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) [0]
#succ(#0) → #pos(#s(#0)) [0]
#succ(#neg(#s(#0))) → #0 [0]
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) [0]
#succ(#pos(#s(@x))) → #pos(#s(#s(@x))) [0]
| times :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #mult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos dyade :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos dyade#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos :: :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos mult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos nil :: :::nil:#0:#s:#neg:#pos mult#1 :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #add :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #0 :: :::nil:#0:#s:#neg:#pos #neg :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #s :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #pred :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #pos :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #succ :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos #natmult :: :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos → :::nil:#0:#s:#neg:#pos |
#add(v0, v1) → null_#add [0]
#mult(v0, v1) → null_#mult [0]
#natmult(v0, v1) → null_#natmult [0]
#pred(v0) → null_#pred [0]
#succ(v0) → null_#succ [0]
dyade#1(v0, v1) → null_dyade#1 [0]
mult#1(v0, v1) → null_mult#1 [0]
null_#add, null_#mult, null_#natmult, null_#pred, null_#succ, null_dyade#1, null_mult#1
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
nil => 1
#0 => 0
null_#add => 0
null_#mult => 0
null_#natmult => 0
null_#pred => 0
null_#succ => 0
null_dyade#1 => 0
null_mult#1 => 0
#add(z, z') -{ 0 }→ @y :|: z' = @y, z = 0, @y >= 0
#add(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#add(z, z') -{ 0 }→ #succ(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #succ(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#add(z, z') -{ 0 }→ #pred(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0
#add(z, z') -{ 0 }→ #pred(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: z = 0, z' = 1 + @y, @y >= 0
#mult(z, z') -{ 0 }→ 0 :|: @x >= 0, z = 1 + @x, z' = 0
#mult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#mult(z, z') -{ 0 }→ 1 + #natmult(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: z' = @y, z = 0, @y >= 0
#natmult(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
#natmult(z, z') -{ 0 }→ #add(1 + @y, #natmult(@x, @y)) :|: @x >= 0, z = 1 + @x, z' = @y, @y >= 0
#pred(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#pred(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#pred(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#pred(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#pred(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
#succ(z) -{ 0 }→ 0 :|: z = 1 + (1 + 0)
#succ(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
#succ(z) -{ 0 }→ 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x))
#succ(z) -{ 0 }→ 1 + (1 + 0) :|: z = 0
#succ(z) -{ 0 }→ 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x)
dyade(z, z') -{ 1 }→ dyade#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
dyade#1(z, z') -{ 1 }→ 1 :|: z' = @l2, z = 1, @l2 >= 0
dyade#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
dyade#1(z, z') -{ 1 }→ 1 + mult(@x, @l2) + dyade(@xs, @l2) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0
mult(z, z') -{ 1 }→ mult#1(@l, @n) :|: @l >= 0, @n >= 0, z' = @l, z = @n
mult#1(z, z') -{ 1 }→ 1 :|: z' = @n, z = 1, @n >= 0
mult#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
mult#1(z, z') -{ 1 }→ 1 + times(@n, @x) + mult(@n, @xs) :|: z' = @n, @x >= 0, z = 1 + @x + @xs, @n >= 0, @xs >= 0
times(z, z') -{ 1 }→ #mult(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0
| eq(start(V, V1),0,[times(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[dyade(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[mult(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun3(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun6(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V1),0,[fun5(V, Out)],[V >= 0]). eq(times(V, V1, Out),1,[fun(V2, V3, Ret)],[Out = Ret,V = V2,V2 >= 0,V1 = V3,V3 >= 0]). eq(dyade(V, V1, Out),1,[fun1(V4, V5, Ret1)],[Out = Ret1,V4 >= 0,V1 = V5,V5 >= 0,V = V4]). eq(fun1(V, V1, Out),1,[mult(V6, V7, Ret01),dyade(V8, V7, Ret11)],[Out = 1 + Ret01 + Ret11,V1 = V7,V6 >= 0,V = 1 + V6 + V8,V7 >= 0,V8 >= 0]). eq(fun1(V, V1, Out),1,[],[Out = 1,V1 = V9,V = 1,V9 >= 0]). eq(mult(V, V1, Out),1,[fun2(V10, V11, Ret2)],[Out = Ret2,V10 >= 0,V11 >= 0,V1 = V10,V = V11]). eq(fun2(V, V1, Out),1,[times(V12, V13, Ret011),mult(V12, V14, Ret12)],[Out = 1 + Ret011 + Ret12,V1 = V12,V13 >= 0,V = 1 + V13 + V14,V12 >= 0,V14 >= 0]). eq(fun2(V, V1, Out),1,[],[Out = 1,V1 = V15,V = 1,V15 >= 0]). eq(fun3(V, V1, Out),0,[],[Out = V16,V1 = V16,V = 0,V16 >= 0]). eq(fun3(V, V1, Out),0,[fun4(V17, Ret3)],[Out = Ret3,V = 2,V1 = V17,V17 >= 0]). eq(fun3(V, V1, Out),0,[fun3(1 + (1 + V18), V19, Ret0),fun4(Ret0, Ret4)],[Out = Ret4,V18 >= 0,V1 = V19,V = 3 + V18,V19 >= 0]). eq(fun3(V, V1, Out),0,[fun5(V20, Ret5)],[Out = Ret5,V = 2,V1 = V20,V20 >= 0]). eq(fun3(V, V1, Out),0,[fun3(1 + (1 + V21), V22, Ret02),fun5(Ret02, Ret6)],[Out = Ret6,V21 >= 0,V1 = V22,V = 3 + V21,V22 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V = 0,V1 = 1 + V23,V23 >= 0]). eq(fun(V, V1, Out),0,[],[Out = 0,V24 >= 0,V = 1 + V24,V1 = 0]). eq(fun(V, V1, Out),0,[fun6(V25, V26, Ret13)],[Out = 1 + Ret13,V25 >= 0,V = 1 + V25,V1 = 1 + V26,V26 >= 0]). eq(fun6(V, V1, Out),0,[],[Out = 0,V1 = V27,V = 0,V27 >= 0]). eq(fun6(V, V1, Out),0,[fun6(V29, V28, Ret14),fun3(1 + V28, Ret14, Ret7)],[Out = Ret7,V29 >= 0,V = 1 + V29,V1 = V28,V28 >= 0]). eq(fun4(V, Out),0,[],[Out = 2,V = 0]). eq(fun4(V, Out),0,[],[Out = 3 + V30,V30 >= 0,V = 2 + V30]). eq(fun4(V, Out),0,[],[Out = 0,V = 2]). eq(fun4(V, Out),0,[],[Out = 2 + V31,V31 >= 0,V = 3 + V31]). eq(fun5(V, Out),0,[],[Out = 2,V = 0]). eq(fun5(V, Out),0,[],[Out = 0,V = 2]). eq(fun5(V, Out),0,[],[Out = 2 + V32,V32 >= 0,V = 3 + V32]). eq(fun5(V, Out),0,[],[Out = 3 + V33,V33 >= 0,V = 2 + V33]). eq(fun3(V, V1, Out),0,[],[Out = 0,V34 >= 0,V35 >= 0,V = V34,V1 = V35]). eq(fun(V, V1, Out),0,[],[Out = 0,V36 >= 0,V37 >= 0,V = V36,V1 = V37]). eq(fun6(V, V1, Out),0,[],[Out = 0,V38 >= 0,V39 >= 0,V = V38,V1 = V39]). eq(fun4(V, Out),0,[],[Out = 0,V40 >= 0,V = V40]). eq(fun5(V, Out),0,[],[Out = 0,V41 >= 0,V = V41]). eq(fun1(V, V1, Out),0,[],[Out = 0,V42 >= 0,V43 >= 0,V = V42,V1 = V43]). eq(fun2(V, V1, Out),0,[],[Out = 0,V44 >= 0,V45 >= 0,V = V44,V1 = V45]). input_output_vars(times(V,V1,Out),[V,V1],[Out]). input_output_vars(dyade(V,V1,Out),[V,V1],[Out]). input_output_vars(fun1(V,V1,Out),[V,V1],[Out]). input_output_vars(mult(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,Out),[V,V1],[Out]). input_output_vars(fun3(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(fun6(V,V1,Out),[V,V1],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(fun5(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun4/2]
1. non_recursive : [fun5/2]
2. recursive [non_tail] : [fun3/3]
3. recursive [non_tail] : [fun6/3]
4. non_recursive : [fun/3]
5. non_recursive : [times/3]
6. recursive : [fun2/3,mult/3]
7. recursive : [dyade/3,fun1/3]
8. non_recursive : [start/2]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun4/2
1. SCC is partially evaluated into fun5/2
2. SCC is partially evaluated into fun3/3
3. SCC is partially evaluated into fun6/3
4. SCC is partially evaluated into fun/3
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into mult/3
7. SCC is partially evaluated into fun1/3
8. SCC is partially evaluated into start/2
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun4/2
* CE 35 is refined into CE [40]
* CE 33 is refined into CE [41]
* CE 34 is refined into CE [42]
* CE 32 is refined into CE [43]
### Cost equations --> "Loop" of fun4/2
* CEs [40] --> Loop 25
* CEs [41] --> Loop 26
* CEs [42] --> Loop 27
* CEs [43] --> Loop 28
### Ranking functions of CR fun4(V,Out)
#### Partial ranking functions of CR fun4(V,Out)
### Specialization of cost equations fun5/2
* CE 38 is refined into CE [44]
* CE 39 is refined into CE [45]
* CE 37 is refined into CE [46]
* CE 36 is refined into CE [47]
### Cost equations --> "Loop" of fun5/2
* CEs [44] --> Loop 29
* CEs [45] --> Loop 30
* CEs [46] --> Loop 31
* CEs [47] --> Loop 32
### Ranking functions of CR fun5(V,Out)
#### Partial ranking functions of CR fun5(V,Out)
### Specialization of cost equations fun3/3
* CE 29 is refined into CE [48]
* CE 25 is refined into CE [49,50,51,52]
* CE 27 is refined into CE [53,54,55,56]
* CE 24 is refined into CE [57]
* CE 26 is refined into CE [58,59,60,61]
* CE 28 is refined into CE [62,63,64,65]
### Cost equations --> "Loop" of fun3/3
* CEs [60,64] --> Loop 33
* CEs [61,65] --> Loop 34
* CEs [58,62] --> Loop 35
* CEs [59,63] --> Loop 36
* CEs [52,56] --> Loop 37
* CEs [51,55] --> Loop 38
* CEs [48,50,54] --> Loop 39
* CEs [49,53] --> Loop 40
* CEs [57] --> Loop 41
### Ranking functions of CR fun3(V,V1,Out)
* RF of phase [33,34,35,36]: [V-2]
#### Partial ranking functions of CR fun3(V,V1,Out)
* Partial RF of phase [33,34,35,36]:
- RF of loop [33:1,34:1,35:1,36:1]:
V-2
### Specialization of cost equations fun6/3
* CE 30 is refined into CE [66]
* CE 31 is refined into CE [67,68,69,70,71,72,73]
### Cost equations --> "Loop" of fun6/3
* CEs [73] --> Loop 42
* CEs [72] --> Loop 43
* CEs [70] --> Loop 44
* CEs [71] --> Loop 45
* CEs [68] --> Loop 46
* CEs [69] --> Loop 47
* CEs [67] --> Loop 48
* CEs [66] --> Loop 49
### Ranking functions of CR fun6(V,V1,Out)
* RF of phase [42,43,44,45,46,47,48]: [V]
#### Partial ranking functions of CR fun6(V,V1,Out)
* Partial RF of phase [42,43,44,45,46,47,48]:
- RF of loop [42:1,43:1,44:1,45:1,46:1,47:1,48:1]:
V
### Specialization of cost equations fun/3
* CE 20 is refined into CE [74,75]
* CE 19 is refined into CE [76]
* CE 17 is refined into CE [77]
* CE 18 is refined into CE [78]
### Cost equations --> "Loop" of fun/3
* CEs [75] --> Loop 50
* CEs [74] --> Loop 51
* CEs [76] --> Loop 52
* CEs [77,78] --> Loop 53
### Ranking functions of CR fun(V,V1,Out)
#### Partial ranking functions of CR fun(V,V1,Out)
### Specialization of cost equations mult/3
* CE 23 is refined into CE [79,80,81]
* CE 21 is refined into CE [82]
* CE 22 is refined into CE [83]
### Cost equations --> "Loop" of mult/3
* CEs [82] --> Loop 54
* CEs [83] --> Loop 55
* CEs [81] --> Loop 56
* CEs [80] --> Loop 57
* CEs [79] --> Loop 58
### Ranking functions of CR mult(V,V1,Out)
* RF of phase [56,57,58]: [V1]
#### Partial ranking functions of CR mult(V,V1,Out)
* Partial RF of phase [56,57,58]:
- RF of loop [56:1]:
V1-1
- RF of loop [57:1]:
V1/2-1/2
- RF of loop [58:1]:
V1
### Specialization of cost equations fun1/3
* CE 16 is refined into CE [84]
* CE 15 is refined into CE [85]
* CE 14 is refined into CE [86,87]
### Cost equations --> "Loop" of fun1/3
* CEs [86] --> Loop 59
* CEs [87] --> Loop 60
* CEs [84] --> Loop 61
* CEs [85] --> Loop 62
### Ranking functions of CR fun1(V,V1,Out)
* RF of phase [59,60]: [V]
#### Partial ranking functions of CR fun1(V,V1,Out)
* Partial RF of phase [59,60]:
- RF of loop [59:1,60:1]:
V
### Specialization of cost equations start/2
* CE 2 is refined into CE [88,89]
* CE 3 is refined into CE [90]
* CE 4 is refined into CE [91]
* CE 5 is refined into CE [92,93,94,95,96,97]
* CE 6 is refined into CE [98,99,100]
* CE 7 is refined into CE [101,102]
* CE 8 is refined into CE [103,104]
* CE 9 is refined into CE [105,106,107,108,109,110,111,112]
* CE 10 is refined into CE [113,114,115]
* CE 11 is refined into CE [116,117]
* CE 12 is refined into CE [118,119,120,121]
* CE 13 is refined into CE [122,123,124,125]
### Cost equations --> "Loop" of start/2
* CEs [109] --> Loop 63
* CEs [107,108] --> Loop 64
* CEs [106] --> Loop 65
* CEs [91] --> Loop 66
* CEs [88,89,90,92,93,94,95,96,97,98,99,100,101,102,103,104,105,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125] --> Loop 67
### Ranking functions of CR start(V,V1)
#### Partial ranking functions of CR start(V,V1)
Computing Bounds
=====================================
#### Cost of chains of fun4(V,Out):
* Chain [28]: 0
with precondition: [V=0,Out=2]
* Chain [27]: 0
with precondition: [Out=0,V>=0]
* Chain [26]: 0
with precondition: [V+1=Out,V>=2]
* Chain [25]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun5(V,Out):
* Chain [32]: 0
with precondition: [V=0,Out=2]
* Chain [31]: 0
with precondition: [Out=0,V>=0]
* Chain [30]: 0
with precondition: [V+1=Out,V>=2]
* Chain [29]: 0
with precondition: [V=Out+1,V>=3]
#### Cost of chains of fun3(V,V1,Out):
* Chain [[33,34,35,36],40]: 0
with precondition: [V1=0,V>=3,Out>=0,V>=Out]
* Chain [[33,34,35,36],39]: 0
with precondition: [V>=3,V1>=0,Out>=0,V>=Out+1]
* Chain [[33,34,35,36],38]: 0
with precondition: [V>=3,V1>=2,Out>=0,V+V1>=Out+1]
* Chain [[33,34,35,36],37]: 0
with precondition: [V>=3,V1>=3,Out>=0,V+V1>=Out+3]
* Chain [41]: 0
with precondition: [V=0,V1=Out,V1>=0]
* Chain [40]: 0
with precondition: [V=2,V1=0,Out=2]
* Chain [39]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [38]: 0
with precondition: [V=2,V1+1=Out,V1>=2]
* Chain [37]: 0
with precondition: [V=2,V1=Out+1,V1>=3]
#### Cost of chains of fun6(V,V1,Out):
* Chain [[42,43,44,45,46,47,48],49]: 0
with precondition: [V>=1,V1>=0,Out>=0]
* Chain [49]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun(V,V1,Out):
* Chain [53]: 0
with precondition: [Out=0,V>=0,V1>=0]
* Chain [52]: 0
with precondition: [V1=0,Out=0,V>=1]
* Chain [51]: 0
with precondition: [Out=1,V>=1,V1>=1]
* Chain [50]: 0
with precondition: [V>=2,V1>=1,Out>=1]
#### Cost of chains of mult(V,V1,Out):
* Chain [[56,57,58],55]: 6*it(56)+3*it(57)+2
Such that:it(57) =< V1/2
aux(7) =< V1
it(56) =< aux(7)
it(57) =< aux(7)
with precondition: [V>=0,V1>=2,Out>=2]
* Chain [[56,57,58],54]: 6*it(56)+3*it(57)+1
Such that:it(57) =< V1/2
aux(8) =< V1
it(56) =< aux(8)
it(57) =< aux(8)
with precondition: [V>=0,V1>=1,Out>=1]
* Chain [55]: 2
with precondition: [V1=1,Out=1,V>=0]
* Chain [54]: 1
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun1(V,V1,Out):
* Chain [[59,60],62]: 7*it(59)+6*s(15)+12*s(16)+1
Such that:aux(11) =< V1
aux(15) =< V
it(59) =< aux(15)
aux(12) =< it(59)*aux(11)
s(18) =< aux(12)* (1/2)
s(15) =< s(18)
s(16) =< aux(12)
s(15) =< aux(12)
with precondition: [V>=2,V1>=0,Out>=2]
* Chain [[59,60],61]: 7*it(59)+6*s(15)+12*s(16)+0
Such that:aux(11) =< V1
aux(16) =< V
it(59) =< aux(16)
aux(12) =< it(59)*aux(11)
s(18) =< aux(12)* (1/2)
s(15) =< s(18)
s(16) =< aux(12)
s(15) =< aux(12)
with precondition: [V>=1,V1>=0,Out>=1]
* Chain [62]: 1
with precondition: [V=1,Out=1,V1>=0]
* Chain [61]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of start(V,V1):
* Chain [67]: 64*s(35)+24*s(38)+48*s(39)+18*s(42)+6*s(61)+12*s(62)+4
Such that:s(60) =< V1/2
aux(19) =< V
aux(20) =< V/2
aux(21) =< V1
s(35) =< aux(19)
s(36) =< s(35)*aux(21)
s(37) =< s(36)* (1/2)
s(38) =< s(37)
s(39) =< s(36)
s(38) =< s(36)
s(42) =< aux(20)
s(42) =< aux(19)
s(61) =< s(60)
s(62) =< aux(21)
s(61) =< aux(21)
with precondition: [V>=0]
* Chain [66]: 1
with precondition: [V=1,V1>=0]
* Chain [65]: 0
with precondition: [V=2,V1=0]
* Chain [64]: 0
with precondition: [V=2,V1>=2]
* Chain [63]: 0
with precondition: [V1=0,V>=3]
Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [67] with precondition: [V>=0]
- Upper bound: 64*V+4+nat(V1)*12+nat(V1)*60*V+9*V+nat(V1/2)*6
- Complexity: n^2
* Chain [66] with precondition: [V=1,V1>=0]
- Upper bound: 1
- Complexity: constant
* Chain [65] with precondition: [V=2,V1=0]
- Upper bound: 0
- Complexity: constant
* Chain [64] with precondition: [V=2,V1>=2]
- Upper bound: 0
- Complexity: constant
* Chain [63] with precondition: [V1=0,V>=3]
- Upper bound: 0
- Complexity: constant
### Maximum cost of start(V,V1): max([1,64*V+4+nat(V1)*12+nat(V1)*60*V+9*V+nat(V1/2)*6])
Asymptotic class: n^2
* Total analysis performed in 599 ms.